Multiple context-free grammars (mcfg's) are a subclass of generalized context-free grammars introduced by Pollard in order to describe the syntax of natural languages. First, this paper shows that the universal recognition problem for mcfg's is EXP-POLY time-complete, where the universal recognition problem is the one to decide whether G generates w for a given grammar G and string w. Next, it is shown that the problem for linear context-free rewriting systems introduced by Vijay-Shanker et al., which is a proper subclass of mcfg's, is PSPACE-complete.

We propose a new decidable subclass of term rewriting systems (TRSs) for which strongly normalizing (SN) property is decidable. The new class is called almost orthogonal inverse finite path overlapping TRSs (AO-FPO-1-TRSs) and the class properly includes AO growing TRSs for which SN is decidable. Tree automata technique is used to show that SN is decidable for AO-FPO-1-TRSs.

This paper proposes an event-based transition system called A-LTS. An A-LTS is a simple system consisting of two agents, a basic program and a monitor. The monitor observes the behavior of the basic program and if the behavior matches some pre-defined pattern, then the monitor interrupts the execution of the basic program and possibly triggers the execution of another specific program. An A-LTS models a common feature found in recent software technologies such as Aspect-Oriented Programming (AOP), history-based access control and active database. We investigate the expressive power of A-LTS and show that it is strictly stronger than finite state machines and strictly weaker than pushdown automata (PDA). This implies that the model checking problem for A-LTS is decidable. It is also shown that the expressive power of A-LTS, linear context-free grammar and deterministic PDA are mutually incomparable. We also discuss the relationship between A-LTS and pointcut/advice in AOP.

This paper proposes a model checking method for microcomputer programs. To deal with the state explosion problem, we adopt a compositional verification approach. Based on the proposed method, a microcomputer program for a real-life air-conditioner is verified. The program is large enough to cause state explosion. Among fourteen typical properties of the program, five properties are successfully verified by our method.

In this paper, we propose an extension of finite state tree automaton, called tree automaton with tree memory (TTA), and also define structure composing TTA (SC-TTA) and backward deterministic TTA (BD-TTA) as subclasses of TTA. We show that the classes of yield languages accepted by TTAs, SC-TTAs and BD-TTAs are equal to the class of recursively enumerable languages, the class of languages generated by tree-to-string finite state translation systems (TSFSTSs) and the class of languages generated by deterministic TSFSTSs, respectively. As a corollary, it is shown that the yield language accepted by an SC-TTA (resp. a BD-TTA) is linear space (resp. polynomial time) recognizable.

Access control is a key technology for providing data security in database management systems (DBMSs). Recently, various authorization models for object-oriented databases (OODBs) have been proposed since authorization models for relational databases are insufficient for OODBs because of the characteristics of OODBs, such as class hierarchies, inheritance, and encapsulation. Generally, an authorization is modeled as a set of rights, where a right consists of at least three components s, o, t and means that subject s is authorized to perform operation t on object o. In specifying authorizations implicitly, inference rules are useful for deriving rights along the class hierarchies on subjects, objects, and operations. An access request req=(s,o,t) is permitted if a right corresponding to req is given explicitly or implicitly. In this paper, we define an authorization model independent of any specific database schemas and authorization policies, and also define an authorization specification language which is powerful enough to specify authorization policies proposed in the literature. Furthermore, we propose an efficient access control method for an authorization specified by the proposed language, and evaluate the proposed method by simulation.

Parallel multiple context-free grammar (PMCFG) and multiple context-free grammar (MCFG) were introduced to denote the syntax of natural languages. By the known fastest algorithm, the recognition problem for multiple context-free language (MCFL) and parallel multiple context-free language (PMCFL) can be solved in O(ne) time and O(ne+1) time, respectively, where e is a constant which depends only on a given MCFG or PMCFG. In this paper, we propose the following two algorithms. (1) An algorithm which reduces the recognition problem for MCFL to the boolean matrices multiplication problem. (2) An algorithm which reduces the recognition problem for PMCFL to the recognition problem for MCFL. The time complexity of these algorithms is O(ne-3i+1 M(ni)) where e and i are constants which depend only on a given MCFG or PMCFG, and M(k) is the time needed for multiplying two k k boolean matrices. The proposed algorithms are faster than the known fastest algorithms unless e=e, i=1 for MCFG, and e=e, i=0 for PMCFG.